$\forall$$T$, $V$:Type, $A$:($T$$\rightarrow\mathbb{P}$), ${\it dcd\_A}$:($t$:$T$$\rightarrow$Dec($A$($t$))), $g$:($T$$\rightarrow$$V$). [$A$? $g$ : $g$] = $g$